FDL - Step of Proof: fun_exp_add-sq

Step of Proof: fun_exp_add-sq

Inference at * 1
Iof proof for Lemma fun exp add-sq:

1. n :

2. 0 < n
3.

m:

, f, x:Top.
3. (primrec((n - 1)+m;

x.x;

i,g. f o g)(x))
3. ~
3. (primrec(n - 1;

x.x;

i,g. f o g)(primrec(m;

x.x;

i,g. f o g)(x)))
4. m :

5. f : Top
6. x : Top

(primrec(n+m;

x.x;

i,g. f o g)(x))

~

(primrec(n;

x.x;

i,g. f o g)(primrec(m;

x.x;

i,g. f o g)(x)))

by ((((RW (AddrC [2;1] (RecUnfoldC `primrec`)) 0)

CollapseTHEN ((((((if (0

C) =0 then SplitOnConclITE else SplitOnHypITE (0))

)
CollapseTHENA (Auto

))

)
CCollapseTHEN (
CC(Try ((Complete (Auto'))

))

))

))

)
CCollapseTHEN (((RW (AddrC [1] (RecUnfoldC `primrec`)) 0)

CCoCollapseTHEN ((((((if (0) =0 then SplitOnConclITE else SplitOnHypITE (0))

)
CollapseTHENA (Auto

Co))

)
CCollapseTHEN ((((Try ((Complete (Auto'))

))

)
CCollapseTHEN (((Reduce 0)
CCollapseTHEN (
CC((EqCD)
CCollapseTHEN ((Try (Trivial))

))

))

))

))

))

))

CC1:

CC1: 7.

(n = 0)
CC1: 8.

(n+m = 0)
CC1:

(primrec((n+m) - 1;

x.x;

i,g. f o g)(x))
CC1:

~
CC1:

(primrec(n - 1;

x.x;

i,g. f o g)(primrec(m;

x.x;

i,g. f o g)(x)))
CC.

Definitions left + right, Unit, i z j, i <z j, p q, p q, p q, [d], a < b, x f y, a < b, null(as), x =a y, P Q, P & Q, x:A B(x), S T, |g|, tt, b, , (i = j), ff, b, n+m, n - m, #$n, SQType(T), P Q, {x:A| B(x)} , {T}, Type, f(a), primrec(n;b;c), x.A(x), f o g, , s = t, t T, A, Top, , x:A. B(x), x:AB(x), a < b, s ~ t,

Lemmas eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, guard wf, top wf